Nuprl Definition : preserved_by
4,23
postcript
pdf
R
preserves
P
==
x
,
y
:
T
.
P
(
x
)
(
x
R
y
)
P
(
y
)
latex
clarification:
preserved_by(
T
;
R
;
P
) ==
x
:
T
,
y
:
T
.
P
(
x
)
(
x
R
y
)
P
(
y
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
x
f
y
FDL editor aliases
preserved_by
origin
x, y:T. P(x) 
(x R y) P(y)
x:T, y:T. P(x) (x R y) P(y) x, y:T. P(x) (x R y) P(y)
x:T, y:T. P(x) (x R y) P(y) x:A. B(x) Q